Issue4163.agda:23,21-25
⊤ !=< ⊥
when checking that the expression unit has type ⊥
